mcsta/modest mcsta zeroconf.jani -E N=1000,K=8,reset=false --props correct_min -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 1e-6 --width 1e-6 --relative-width
zeroconf.jani:model: info: zeroconf is an MDP model.
zeroconf.jani:variables[21]: info: Expanding variable "l" into 5 locations in automaton "host0".
zeroconf.jani: info: Need 24 bytes per state.
zeroconf.jani: info: Explored 1868787 states for N=1000, K=8, reset=False.
Peak memory usage: 710 MB
Analysis results for zeroconf.jani
Experiment N=1000, K=8, reset=False
+ State space exploration
State size: 24 bytes
States: 1868787
Transitions: 3430379
Branches: 4224736
Rate: 387394 states/s
Time: 5.1 s
+ Property correct_min
Probability: 5.040105212929842E-09
Bounds: [5.040105212929842E-09, 5.040105212929842E-09]
Time: 10.8 s
+ Essential states
Iterations: 37
Essential states: 1312763
Transitions: 2800966
Branches: 3572836
Time: 4.8 s
+ Optimistic value iteration
Total iterations: 69
Verif. attempts: 1
Verif. iterations: 9
Final epsilon: 1E-06
Time: 5.9 s
Exported results to file "/out.txt".